| Definitions | x:A  B(x), P   Q, P  Q,  x:A. B(x), Knd, x:A  B(x), P & Q, P Q, triggersGlue(A; l; tg; ds; conds), Type, t  T, IdLnk, Id,   x. t(x), a:A fp B(a), Top, left + right, State(ds), x.A(x), source(l), hasloc(k;i),  b, KindDeq, x dom(f), Normal(ds), Normal(T), rcv(l,tg), s = t,  ,  A, f(x), t.1, fpf-domain(f), (x l), R-Feasible(R), {x:A| B(x)} , trigger-send(A;ds;x;cond;l;tg),  xL.R(x), [], [car / cdr], Atom$n, if b then t else f fi , xdom(f). v=f(x) P(x;v), False, let x,y = A in B(x;y), {T}, type List, a < b, EqDecider(T), Rsframe(lnk;tag;L), Realizer, {i..j }, A  B, i j < k,  , es realizer ind Rsends compseq tag def, es realizer ind Rsframe compseq tag def, Rinit-v(x1), Rinit-x(x1), Rinit?(x1), Reffect-f(x1), Reffect-x(x1), Reffect?(x1), Rinit-discrete(A), Reffect-discrete(A), R-discrete_compat(A;B), x : v, <a, b>, Rsends(ds;knd;T;l;dt;g),  b,  , tag(k), IdDeq, f g, Unit, True, lnk-decl(l;dt), Void,  x:A.B(x), S  T, isrcvl(l;k), f || g, SQType(T), s ~ t, a = b, (i = j), Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), inr x , A || B,  x:A. B(x), hd(l), i <z j, i z j, l[i], tl(l), P  Q, Dec(P), (x,yL. P(x;y)), A c B,  , ||as||, xL. P(x), ff, tt, if a=1 b then x else y, case b of inl(x) => s(x) | inr(y) => t(y), lnk(k), a = b, f(x)?z, f(a),  T, x,y. t(x;y), a = b, es realizer ind, rec(x.A(x)), DeclaredType(ds;x), #$n |
| Lemmas | R-Feasible wf, length wf1, select wf, fpf-join-dom-sq, assert of bor, IdLnk sq, lnk-decls-compatible, fpf-single-dom, fpf-compatible-join, fpf-compatible-singles, fpf-compatible-join2, fpf-compatible-symmetry, lnk-decl-compatible-single, fpf-compatible-self, bool sq, assert-eq-knd, fpf-all-join-decl, fpf-all-single-decl, fpf-all-single, isrcv-implies, squash wf, true wf, fpf-single-dom-sq, fpf-cap-single, fpf-cap-single1, fpf-join-cap-sq, eq lnk wf, lnk wf, assert-hasloc, R-feasible-Rall, decidable equal Kind, Rds wf, fpf-compatible wf, Rda wf, eq bd wf, R-base-domain wf, R-frame-compat wf, R-discrete compat wf, R-interface-compat wf, btrue wf, bfalse wf, R-compat wf, nat wf, Knd sq, length wf nat, assert-isrcvl, decidable int equal, R-compat-Rall, R-compat-disjoint, R-compat-symmetry, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, Id sq, id-deq wf, fpf-empty-compatible-left, isrcvl wf, fpf-single wf, lnk-decl wf, ifthenelse wf, fpf-join wf, fpf-single wf3, tagof wf, assert-eq-lnk, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, es realizer wf, Rsframe wf, Rall wf, trigger-send wf, member-fpf-dom, all functionality wrt iff, implies functionality wrt iff, R-feasible-Rlist, l member wf, fpf-domain wf, pi1 wf, fpf-ap wf, not wf, rcv wf, normal-type wf, normal-ds wf, fpf-dom wf, Kind-deq wf, assert wf, hasloc wf, lsrc wf, fpf-trivial-subtype-top, decl-state wf, top wf, Knd wf, fpf wf, Id wf, IdLnk wf, member-fpf-domain |